ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:ecl(ds; da), es:event_system{i:l}, i:Id.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). (loc(e) = i)  subtype_rel(es-valtype(es; e); ma-valtype(da; es-kind(es; e))))
 (m:. 
 ecl-es-act(es; m; x)  {e:es-E(es)| loc(e) = i} {e:es-E(es)| loc(e) = i} prop{i:l}) 

latex

Definitions

ff, tt, x,y,z. t(x;y;z), subtype(S; T), A  B, x:A. B(x), , (x  l), x. t(x), A c B, x,y,z,w. t(x;y;z;w), x,y. t(x;y), if b then t else f fi , A, P  Q, P  Q, False, ecl-es-act(es; m; x), prop{i:l}, t  T, , P  Q, x:A. B(x), P  Q, Unit, x(s), x(s1,s2,s3), x(s1,s2,s3,s4), x(s1,s2), ,

Lemmas

Knd wf, fpf wf, ecl wf, event system wf, top wf, id-deq wf, fpf-cap wf, es-vartype wf, es-kind wf, es-valtype wf, Id wf, es-E wf, nat wf, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, assert of eq int, eqtt to assert, iff transitivity, es-pstar-q wf, nat plus inc, ecl-ex wf, le wf, alle-between1 wf, select wf, length wf1, l-all wf, es-loc-pred, es-pred wf, es-first wf, assert wf, not wf, existse-between3 wf, ecl-es-halt wf, bool wf, ma-valtype wf, decl-state wf, false wf, es-loc wf, ecl ind wf